# -*- coding: utf-8 -*-
import re, random, os, os.path, sys, copy

TOP_OF_THE_STACK = -1

class LTSError (Exception):
	"""
		Clase de excepcion para este módulo.
	"""
	pass

class Alphabet:
	"""
		Esta clase reprecenta el alfabeto de un LTS.
	"""
	
	def __init__ (self):
		self.sets = dict()
		# Conjunto de eventos observables.
		self.sets['o'] = set()
		# Conjunto de eventos no observables.
		self.sets['u'] = set()
		# Conjunto de eventos de falla.
		self.sets['f'] = set()
		# Conjunto de eventos de sincronizacion.
		self.sets['c'] = set()
	
	def __copy__ (self):
		result = Alphabet()
		result.sets['o'] = set(self.sets['o'])
		result.sets['u'] = set(self.sets['u'])
		result.sets['f'] = set(self.sets['f'])
		result.sets['c'] = set(self.sets['c'])
		return result
	
	#	Para las siguientes funciones los posibles valores para el argumento
	# 'event_type' son:
	#		'o'	=>	Conjutno de eventos observables.
	#		'u'	=>	Conjunto de eventos no observables.
	#		'f'	=>	Conjunto de eventos de falla.
	#		'c'	=>	Conjunto de eventos de sincronizacion.
	#	En caso de proporcionar un valor incorrecto se produce una excepcion
	# de tipo LTSError.
	
	def is_event (self, event, event_type):
		"""
			Dice si el evento 'event' existe en el conjunto de eventos indicado
			por 'event_type'.
		"""
		try:
			return event in self.sets[event_type]
		except KeyError:
			raise LTSError("Incorrect type event:", event_type)
	
	def add_event (self, event, event_type):
		"""
			Agrega el evento 'event' al conjunto de eventos indicado por
			'event_type'.
		"""
		try:
			(self.sets[event_type]).add(event)
		except KeyError:
			raise LTSError("Incorrect type event:", event_type)
	
	def remove_event (self, event, event_type):
		"""
			Elimina el evento 'event' del conjunto de eventos indicado por
			'event_type'.
		"""
		try:
			(self.sets[event_type]).remove(event)
		except KeyError:
			raise LTSError("Incorrect type event", event_type)
	
	def get_event_set (self, event_type):
		"""
			Devuelve el conjunto de eventos indicado por 'event_type'.
			NOTA: Se devuelve una referencia al conjunto, no una copia de el.
		"""
		try:
			return self.sets[event_type]
		except KeyError:
			raise LTSError("Incorrect type event", event_type)
	
	def union (self, alphabet):
		result = Alphabet()
		result.sets['o'] = self.sets['o'].union(alphabet.sets['o'])
		result.sets['u'] = self.sets['u'].union(alphabet.sets['u'])
		result.sets['f'] = self.sets['f'].union(alphabet.sets['f'])
		result.sets['c'] = self.sets['c'].union(alphabet.sets['c'])
		return result

class State:
	"""
		Esta clase reprecenta un estado de un LTS.
	"""
	
	def __init__ (self, name='', init=False):
		### Atributos Privados ###
		# Relacion de vecino. Es un conjunto de tuplas=(event,state).
		self.neighbors = set()
		### Atributos Publicos ###
		# Nombre del estado.
		self.name = name
		# Dice si es el estado inicial o no.
		self.init = init
		# Informacion de fallas
		self.fault_info = None
		# Informacion de estados (Izquierdo,Derecho).
		self.left_state = None
		self.right_state = None
		# Dice si fue visitado o no.
		self.visited = False
	
	def __eq__ (self, y):
		result = False
		if y == None:
			result = False
		else:
			result = (self.fault_info == y.fault_info) and \
					 (self.left_state == y.left_state) and \
					 (self.right_state==y.right_state) and (self.name==y.name)
		return result
	
	def __str__ (self):
		result = self.name
		if self.left_state!=None and self.right_state!=None:
			result += '#L('
			if self.left_state.fault_info:
				for f in self.left_state.fault_info:
					if result.endswith('('):
						result += f
					else:
						result += ','+f
			result += ')#R('
			if self.right_state.fault_info:
				for f in self.right_state.fault_info:
					if result.endswith('('):
						result += f
					else:
						result += ','+f
			result += ')'
		elif self.fault_info != None:
			result += '#('
			for f in self.fault_info:
				if result.endswith('('):
					result += f
				else:
					result += ','+f
			result += ')'
		else:
			pass
		return result
	
	def __hash__ (self):
		return self.name.__hash__()
	
	### Proyectores para el nombre.
	
	def set_name (self, name):
		self.name = name
	
	def get_name (self):
		return self.name
	
	### Proyectores para la relacion de vecino.
	
	def is_neighbor (self, neighbor, event=None):
		"""
			Dice si el estado 'neighbor' esta relacionado con 'self'.
			
			Mas formalmente:
				self.is_neighbor(n,e)=True <==> Exist (n',e') € self.neighbors :
				n=n' and (e=e' or e=None)
		"""
		xs = [t[1] for t in self.neighbors \
				if t[1]==neighbor and (not event or t[0]==event)]
		return neighbor in xs
	
	def add_neighbor (self, event, neighbor):
		"""
			Agrega un estado a la relacion de vecinos de 'self'.
		"""
		self.neighbors.add((event,neighbor))
	
	def remove_neighbor (self, event, neighbor):
		"""
			Elimina un estado de la relacion de vecinos de 'self'.
		"""
		self.neighbors.remove((event,neighbor))
	
	def get_neighbor_set (self):
		"""
			Devuelve el conjunto de relacion de vecinos de 'self'.
			NOTA: Devuelve una referencia al conjunto, no una copia de el.
		"""
		return self.neighbors
	
	### Proyectores para el indicador de estado incial.
	
	def set_init_state (self, init):
		self.init = init
	
	def is_init_state (self):
		return self.init
	
	### Proyectores para la informacion de fallas.
	
	def add_fault_info (self, f):
		"""
			Agregala falla 'f' al conjunto de fallas del estado.
		"""
		if self.fault_info == None:
			self.fault_info = set()
		self.fault_info.add(f)
	
	def get_fault_info (self):
		"""
			Devuelve el conjunto de fallas del estado.
			NOTA: Devuelve una referencia al conjunto, no una copia de el.
		"""
		if self.fault_info != None:
			return self.fault_info
		else:
			return set()

class LTS:
	"""
		Esta clase reprecenta un Labelled Transition System.
	"""
	
	def __init__ (self, init_state=None):
		### Atributos Privados ###
		self.alphabet = Alphabet()
		self.states = set()
		self.twinplant = None
		self.recalc_tp = True
		### Atributos Publico ###
		self.init_state = init_state
		self.name = 'LTS-'+str(int(random.random()*100))
		self.isdiag = None
	
	### Funciones para los estados.
	
	def add_state(self, s):
		self.states.add(s)
		if s.init:
			self.init_state = s
		self.recalc_tp = True
	
	def remove_state (self, s):
		self.states.remove(s)
		if s.init:
			self.init_state = None
		self.recalc_tp = True
	
	def is_state (self, s):
		return s in self.states
	
	def get_states_by_name (self, state_name):
		"""
			Devuelve una lista de estados con el mismo nombre.
		"""
		return [s for s in self.states if s.name == state_name]
	
	def get_state (self, state):
		for x in self.states:
			if x == state:
				return x
		return None
	
	def get_init_state (self):
		if self.init_state:
			return self.init_state
		else:
			raise LTSError("Initial state not established.")
	
	def get_state_set (self):
		return self.states
	
	def get_state_count (self):
		return len(self.states)
	
	### Funciones para los eventos.
	
	def is_event (self, event, event_type):
		return self.alphabet.is_event(event, event_type)
	
	def add_event (self, event, event_type):
		self.alphabet.add_event(event, event_type)
		self.recalc_tp = True
	
	def remove_event (self, event, event_type):
		self.alphabet.remove_event(event, event_type)
		self.recalc_tp = True
	
	def get_event_set (self, event_type):
		return self.alphabet.get_event_set(event_type)
	
	### Funciones para las transiciones.
	
	def add_transition (self, s_from, event, s_to):
		"""
			Agrega una transicion entre dos estados.
			Los estados 's_from' y 's_to' deben existir en el LTS.
		"""
		# Me fijo si existen los estados.
		if not self.is_state(s_from):
			raise LTSError("Source state not found", s_from.name)
		else:
			s_from = self.get_state(s_from)
		if not self.is_state(s_to):
			raise LTSError("Destination state not found", s_to.name)
		else:
			s_to = self.get_state(s_to)
		s_from.add_neighbor(event, s_to)
		self.recalc_tp = True
	
	def remove_transition (self, s_from, event,  s_to):
		"""
			Elimina una transicion entre dos estados.
			Los estados 's_from' y 's_to' deben existir en el LTS.
		"""
		# Me fijo si existen los estados.
		if not self.is_state(s_from):
			raise LTSError("Source state not found", s_from.name)
		else:
			s_from = self.get_state(s_from)
		if not self.is_state(s_to):
			raise LTSError("Destination state not found", s_to.name)
		else:
			s_to = self.get_state(s_to)
		s_from.remove_neighbor(event, s_to)
		self.recalc_tp = True
	
	def get_transition_set (self):
		"""
			Devulve un conjunto de pares de la forma (n,e,n') indicando que hay
			una transicion de la forma n -e-> n'.
		"""
		x = [(s,t[0],t[1]) for s in self.states for t in s.get_neighbor_set()]
		return set(x)
	
	def exist_transition (self, s_from, event, s_to):
		"""
			Dice si existe una transicion de la forma  "s_from -e-> s_to".
		"""
		x = (s_from, event, s_to)
		return x in [(s,t[0],t[1]) for s in self.states \
					for t in s.get_neighbor_set()]
	
	### Operadores.
	
	def get_diagnoser (self, label=''):
		# Creo el Diagnoser.
		diagnoser = LTS()
		# Busco el estado inicial de 'self'.
		s0 = self.get_init_state()
		# Creo el estado inicial del diagnoser.
		d0 = State(s0.name, True)
		d0.fault_info = set()
		# Agrego el estado inicial del diagnoser.
		diagnoser.add_state(d0)
		# Quien Agrego a Quien! (Who Added Who)
		waw = dict()
		# Creo la cola para hacer BFS.
		queue = [(d0,d0,d0)]
		# Mientras no se vacie la cola...
		while queue:
			# Tomo el primer elemento de la cola.
			dstate,pre_dstate,bstate = queue.pop(0)
			# Agrego los vecinos no visitados de 'dstate'.
			state = self.get_states_by_name(dstate.name)[0]
			for e,s in state.get_neighbor_set():
				new_dstate = State(s.name, False)
				new_dstate.fault_info = set(dstate.fault_info)
				# Si el evento es una falla la agrego al conjunto de fallas.
				if self.is_event(e, 'f'):
					new_dstate.fault_info.add(e)
				# Me fijo si el estado ya existe en el diagnoser.
				if diagnoser.is_state(new_dstate): # Si ya existe, lo tomo. 
					new_dstate = diagnoser.get_state(new_dstate)
				else: # Si no existe lo agrego.
					diagnoser.add_state(new_dstate)
				# Si es observable tengo que agregar la transicion al diagonser.
				if self.is_event(e, 'o'):
					diagnoser.add_transition(pre_dstate, e, new_dstate)
					diagnoser.add_event(e, 'o')
					new_pre_dstate = new_dstate
				else:
					new_pre_dstate = pre_dstate
				if not waw.has_key(str(dstate)):
					waw[str(dstate)] = []
				if (new_dstate,bstate) in waw[str(dstate)]:
					continue
				else: # Si no, lo agrego a la cola.
					queue.append((new_dstate,new_pre_dstate,dstate))
					waw[str(dstate)].append((new_dstate,bstate))
			# Marco el estado como visitado.
			dstate.visited = True
		# Elimino los estados que no tienen transiciones salientes.
		self._remove_deadlock_states(diagnoser)
		# Le ponemos un nombre al diagnoser.
		if label: diagnoser.name = '('+label+')'+'-diagnoser-'+self.name
		else: diagnoser.name = 'diagnoser-'+self.name
		return diagnoser
	
	def get_twinplant (self):
		"""
			Devuelve la twnplant de 'self'.
			Si es necesario la recalcula.
		"""
		if self.recalc_tp:
			# Creo el diagnoser "izquierdo".
			left_diagnoser = self.get_diagnoser('L')
			# Creo el diagnoser "derecho".
			right_diagnoser = self.get_diagnoser('R')
			# Sincronizo en los eventos observables.
			sync_set = self.get_event_set('o')
			# Creo la twinplant sincronizando los Dagnoser.
			self.twinplant = left_diagnoser.sync(right_diagnoser, sync_set, None, True)
			# Le ponemos un nombre a la twinplant.
			self.twinplant.name = 'twinplant-'+self.name
			self.recalc_tp = False
		return self.twinplant
	
	def sync (self, g, sync_set=None, name=None, state_ref=False, rm_dstates=True):
		"""
			Calcula y devuelve la composicion en paralelo entre el sistema
			'self' y 'g'.
			Por defecto se sincroniza en el conjunto de eventos de
			sincronizacion.
			Descripcion de los argumentos:
			~ sync_set: Es el conjunto de eventos de sincronizacion.
			~ name: Permite especificar un nombre para el nuevo sistema.
			~ state_ref: Dice si se eliminan o no las referencias de cada estado
			  del nuevo sistema a los estados de los sistemas anteriores. 
			  Basicamente un estado en un sistema compuesto esta formado por la 
			  union de dos estados de los sistemas a componer, este flag permite 
			  decidir si la referencia a esos estados se guarda o no.
			~ rm_dstates: Este flag le dice al algoritmo de composicion si tiene
			  que eliminar los 'deadlock states' luego de la composicion.
		"""
		sync_set = self._calculate_sync_set(g, sync_set)
		# Creo el LTS resultante.
		lts = LTS()
		# Creo el alfabateo.
		lts.alphabet = self.alphabet.union(g.alphabet)
		# Cola para hacer BFS.
		queue = []
		# Creo el estado inicial.
		x = self.get_init_state()
		y = g.get_init_state()
		s = State(x.name+'-'+y.name, True)
		s.left_state = x
		s.right_state = y
		# Lo agrego al LTS.
		lts.add_state(s)
		# Lo pongo en la cola.
		queue.append(s)
		# Mientras no sea vacia la cola...
		while queue:
			# Tomo al prmer elemento de la cola.
			state = queue.pop(0)
			# Busco vecinos para ese elemento.
			self._sync_search_transition(state, queue, lts, sync_set)
		# Le ponemos un nombre al lts.
		if name: lts.name = name
		else: lts.name = (self.name.replace('.aut', ''))+'-'+g.name
		# Elimino la referencia a los estados.
		if not state_ref:
			for state in lts.get_state_set():
				state.left_state = None
				state.right_state = None
		# Elimino los estados que no tienen transiciones salientes.
		lts = self._remove_deadlock_states(lts)
		return lts
	
	def is_diagnosable (self, fault_set, verbose=False):
		result = dict()
		result['is_diag'] = True
		result['fault_list'] = [] 
		twinplant = self.get_twinplant()
		to_file(twinplant)
		fault_set = self.get_event_set('f').intersection(fault_set)
		for f in fault_set:
			path = self._find_undecidible_path(twinplant, f)
			if not path == []:
				result['is_diag'] = False
				result['fault_list'].append((f,path))
				if verbose: print '   ',f,"is non-diagnosable."
			else:
				if verbose: print '   ',f,"is diagnosable."
		return result
	
	def list_paths (self):
		# Lista donde voy a almacenar los caminos.
		path_list = []
		# Preparo la pila para hacer DFS. Los elementos de la pila seran de la forma
		# (S,E,L) donde S es un estado, E es el evento con el que se puso a S en la
		# pila, y L es la lista de vecinos visitado de S.
		stack = []
		# Tomo el estado incial del sistema
		s0 = self.get_init_state()
		# Pongo el primer elemento de la pila.
		stack.append((s0,'',[]))
		# Cuenta la cantidad de caminos.
		i = 0
		# Mientras no se vacie la pila.
		while stack:
			# Apunto al tope de la pila (no hago pop).
			state,event,visited_list = stack[TOP_OF_THE_STACK]
			# Flag para saber si recorri todos los vecinos de 'state'.
			visit_all_neighbors = True
			# Recorro los vecinos de 'state'.
			for e,x in state.get_neighbor_set():
				# Si el estado ya fue visitado busco el siguiente.
				if (e,x) in visited_list: continue
				# Si no fue visitado me fijo si esta en la pila.
				if x in [t[0] for t in stack]:
					i += 1
					if i % 10000 == 0:
						os.write(1,str(i)+'\r')
					# Si esta en la pila ==> Encontre un ciclo.
					# Pongo a 'x' en la pila.
					stack.append((x,e,[]))
					# Convierto la pila en un camino y lo agrego a la lista.
					path_list.append(stack_to_path(stack))
					# Saco a 'x' de la pila y sigo.
					stack.pop()
				else:
					# Si no fue visitado y no estaba en la pila lo pongo como
					# visitado, lo pongo en la pila y comienzo de nuevo el ciclo.
					visited_list.append((e,x))
					stack.append((x,e,[]))
					visit_all_neighbors = False
					break
			# Me fijo si sali porque visite a todos los vecinos de 'state' o porque
			# puse a alguien nuevo en la pila.
			if visit_all_neighbors:
				# Si visite a todos los vecinos saco a 'state' de la pila.
				stack.pop()
		# Total de caminos.
		print "Total de caminos:", str(i)
		return path_list
	
	def reduce_by_faults (self, fault_set):
		# Tomo el conjunto de estados del sistema.
		states = self.get_state_set()
		# Lista de transiciones a eliminar.
		deleted_transitions = []
		# Para cada estado reviso sus transiciones salientes.
		for state in states:
			# Obtengo la relacion de vecino.
			neighbors = state.get_neighbor_set()
			for t in neighbors:
				if t[0] in fault_set:
					deleted_transitions.append(t)
		# Ahora tengo que armar el nuevo sistema.
		reduced_system = LTS()
		# Copio el alfabeto.
		reduced_system.alphabet = self.alphabet.__copy__()
		# Creo el estado inicial.
		init_state = State(self.get_init_state().name, True)
		reduced_system.add_state(init_state)
		# Cola para hacer BFS.
		queue = []
		# Pongo el estado inicial en la cola.
		queue.append(init_state)
		# Mientras no sea vacia la cola...
		while queue:
			# Tomo al primer elemento de la cola.
			state = queue.pop(0)
			if state.visited:
				continue
			# Lo marco como visitado.
			state.visited = True
			# Busco el estado correspondiente el 'self'.
			self_state = self.get_states_by_name(state.name)[0]
			# Agrego los vecinos de ese estado.
			neighbors = self_state.get_neighbor_set()
			for (e,s) in neighbors:
				if not (e,s) in deleted_transitions:
					new_state = reduced_system.get_states_by_name(s.name)
					if new_state == []:
						new_state = State(s.name, False)
						reduced_system.add_state(new_state)
					else:
						new_state = new_state[0]				
					reduced_system.add_transition(state,e,new_state)
					if not new_state.visited:
						queue.append(s)
		# Le ponemos un nombre a reduced_system.
		reduced_system.name = 'R'+(self.name.replace('.aut', ''))
		# Devolvemos el sitema reducido.
		return reduced_system

	def _find_undecidible_path (self, twinplant, fault):
		# Busco el estado inicial de la twinplant.
		s0 = twinplant.get_init_state()
		# Creo la pila para hacer DFS. Los elementos de la pila seran ternas de la
		# forma (s,e,l) donde: 's' es un estado, 'e' es el evento con el que se puso
		# a 's' en la pila, y 'l' es la lista de vecinos visitadoa de 's'.
		stack = [(s0,'',[])]
		# Flag para la terminacion del cliclo.
		find_path = False
		# Hago DFS para buscar el camino.
		while not find_path and stack:
			# Apunto al tope de la pila (no hago pop).
			state,event,visited_list = stack[TOP_OF_THE_STACK]
			# Flag para saber si recorri todos los vecinos de 'state'.
			visit_all_neighbors = True
			# Recorro los vecinos de 'state'.
			for e,x in state.get_neighbor_set():
				# Si el estado ya fue visitado busco el siguiente.
				if x in visited_list: continue
				# Si no fue visitado me fijo si esta en la pila.
				if x in [t[0] for t in stack]:
					# Si esta en la pila ==> Encontre un ciclo.
					# Pongo a 'x' en la pila.
					stack.append((x,e,[]))
					# Me fijo si es un camino indecidible para 'fault'.
					if self._is_undecidible_path(stack,fault):
						# Encontre lo que buscaba !!!
						visit_all_neighbors = False
						find_path = True
						break
					else:
						# Si no, saco a 'x' de la pila y sigo.
						stack.pop()
						# Pongo a 'x' en la lista de visitados de 'state'.
						visited_list.append(x)
				else:
					# Si no fue visitado y no estaba en la pila lo pongo como
					# visitado y lo pongo en la pila.
					visited_list.append(x)
					stack.append((x,e,[]))
					visit_all_neighbors = False
					break
			# Me fijo si sali porque visite a todos los vecinos de 'state' o porque
			# puse a alguien nuevo en la pila.
			if visit_all_neighbors:
				# Si visite a todos los vecinos saco a 'state' de la pila.
				stack.pop()
		# Si encontre un camino indecidible armo la lista que voy a retornar.
		if find_path:
			return stack_to_path(stack)
		else:
			return []

	def _is_undecidible_path (self, path, fault):
		"""
			Dice si el camino 'path' es indecidible para 'fault' o no.
		"""
		# Dice si todos los estados del ciclo son indecidibles o no.
		all_states_undecidible = True
		# Dice si hay o no al menos un evento observable dentro del ciclo.
		exist_observable_event = False
		# Tomo el ultimo estado del camino.
		last_state = (path[-1])[0]
		for i in range(1, len(path)+1):
			# Para recorrer 'path' de atras hacia adelente.
			i *= -1
			# Leo el estado y el evento.
			state,event,l = path[i]
			# Me fijo si el evento es observable.
			if event.startswith('o'):
				exist_observable_event = True
			# Me fijo si el estado es indecidible.
			if not self._is_undecidible_state(state, fault):
				all_states_undecidible = False
			# Si llego a un estado identico al ultimo estado, es porque recorri todo
			# el ciclo ==> Termino.
			if state == last_state:
				break
		if all_states_undecidible and exist_observable_event:
			return True
		else:
			return False

	def _is_undecidible_state (self, state, fault):
		"""
			Dice si un estado es indecidible para una determinada falla.
		"""
		left_fault_info = state.left_state.get_fault_info()
		right_fault_info = state.right_state.get_fault_info()
		s1 = left_fault_info.union(right_fault_info)
		s2 = left_fault_info.intersection(right_fault_info)
		if (fault in s1 and not fault in s2) or (not fault in s1 and fault in s2):
			return True
		else:
			return False
		
	def _remove_deadlock_states(self, lts):
		finished = False
		while not finished:
			states_to_remove = set([])
			for s1 in lts.get_state_set():
				# Si tiene transiciones salientes, o es el estado inicial, sigo 
				# con el sieguieinte estado.
				if s1.get_neighbor_set() or s1.init: continue
				# Si no, lo elimino de la lista de vecinos de los demas estados.
				for s2 in lts.get_state_set():
					# Si no tiene a s1 como vecino, sigo con el sieguiente.
					if not s2.is_neighbor(s1): continue
					# Si lo tiene como vecino, elimino todas las transiciones.
					nb = s2.get_neighbor_set()
					s2.neighbors = set([t for t in nb if t[1]!=s1])
				states_to_remove.add(s1)
			if states_to_remove:
				for s in states_to_remove:
					if not s.init:
						lts.remove_state(s)
			else:
				finished = True
		return lts
	
	def _calculate_sync_set (self, g, sync_set):
		if sync_set == None:
			slef_events = self.get_event_set('o')
			g_events = g.get_event_set('o')
			sync_set = slef_events.intersection(g_events)
		else:
			o_self_events = self.get_event_set('o')
			o_g_events = g.get_event_set('o')
			o_sync_set = o_self_events.intersection(o_g_events)
			sync_set = sync_set.intersection(o_sync_set)
		return sync_set
	
	def _sync_search_transition (self, state, queue, lts, sync_set):
		"""
			Funcion interna. Agrega transiciones a un lts de sincronizacion.
		"""
		x = state.left_state
		y = state.right_state
		# Recorremos todos los vecinos de 'x'.
		for (e1,n1) in x.get_neighbor_set():
			if not e1 in sync_set:
				# Si el evento de la transicion no es de sincronizacion, me
				# puedo mover al otro estado sin problemas.
				# Busco el estado de llegada.
				s_to = State(n1.name+'-'+y.name, n1.init and y.init)
				s_to.left_state = n1
				s_to.right_state = y
				# Si no esta en el lts lo agregamos.
				if not lts.is_state(s_to): lts.add_state(s_to)
				else: s_to = lts.get_state(s_to)
				# Agrego la transicion.
				lts.add_transition(state, e1, s_to)
				lts.add_event(e1, e1[0])
				# Si no fue visitado lo encolamos.
				if not s_to.visited:
					s_to.visited = True
					queue.append(s_to)
			else:
				# Si el evento es de sincronizacion entonces debo ver si el 
				# estado 'y' tiene alguna transicion con ese evento.
				for (e2,n2) in y.get_neighbor_set():
					if e1 == e2:
						# Busco el estado de destino.
						n_to = n1.name+'-'+n2.name
						s_to = State(n_to, n1.init and n2.init)
						s_to.left_state = n1
						s_to.right_state = n2
						if not lts.is_state(s_to): lts.add_state(s_to)
						else: s_to = lts.get_state(s_to)
						lts.add_transition(state, e2, s_to)
						lts.add_event(e2, e2[0])
						# Si no fue visitado lo encolamos.
						if not s_to.visited:
							s_to.visited = True
							queue.append(s_to)
		# Recorremos todos los vecinos de 'y'.
		for (e1,n1) in y.get_neighbor_set():
			if not e1 in sync_set:
				# Si el evento de la transicion no es de sincronizacion, me
				# puedo mover al otro estado sin problemas.
				# Bsco el estado de destino.
				s_to = State(x.name+'-'+n1.name, x.init and n1.init)
				s_to.left_state = x
				s_to.right_state = n1
				if not lts.is_state(s_to): lts.add_state(s_to)
				else: s_to = lts.get_state(s_to)
				lts.add_transition(state, e1, s_to)
				lts.add_event(e1, e1[0])
				# Si no fue visitado lo encolamos.
				if not s_to.visited:
					s_to.visited = True
					queue.append(s_to)
			else:
				for (e2,n2) in x.get_neighbor_set():
					if e1 == e2:
						# Busco el estado de destino.
						n_to = n2.name+'-'+n1.name
						s_to = State(n_to, n2.init and n1.init)
						s_to.left_state = n2
						s_to.right_state = n1
						if not lts.is_state(s_to): lts.add_state(s_to)
						else: s_to = lts.get_state(s_to)
						lts.add_transition(state, e2, s_to)
						lts.add_event(e2, e2[0])
						# Si no fue visitado lo encolamos.
						if not s_to.visited:
							s_to.visited = True
							queue.append(s_to) 

### Funciones del modulo ###

def stack_to_path (stack):
	"""
		Convierte una pila con determinado formato en un camino.
	"""
	result = []
	for (s,e,l) in stack:
		if e != '':
			result.append(e)
		result.append(s)
	return result

def path_to_string (t, maps_dict=None):
	"""
		Convierte un camino en una cadena de texto.
		Args : ( (path,system), dict(dict(),...,dict()) )
		Toma como primer argumento una tupla que contiene al 'path' en la primer 
		coordenada y al sistema al que pertenece en la segunda coordenada. El 
		segundo es un diccionario de deccionarios de mapeos, que mapean los 
		nombres de los estados a numeros, esos diccionarios son los devueltos 
		por la funcion 'lts.to_file()'.
	"""
	# Hago una copia del camino de 't'.
	path = list(t[0])
	# Tomo la componente.
	g = t[1]
	# Busco el mapeo para 'path'.
	if maps_dict:
		map_info = maps_dict[g]
	# Convierto a 'path' en un string
	for i in range(0,len(path)):
		if i%2 == 0:
			if maps_dict:
				state_name = map_info[str(path[i])]
			else:
				state_name = str(path[i])
			path[i] = '('+state_name+')'
		else:
			path[i] = '"'+str(path[i])+'"'
	separator = ' -> '
	return separator.join(path)+'\t['+g.name+']'

def tp_to_sys_path (t, maps_dict=None):
	"""
		Transforma un camino de una twinplant en la parte observable de dos
		caminos del sistema al que corresponde la twinplant.
	"""
	# Hago una copia del camino de 't'.
	pathL = list(t[0])
	pathR = list(t[0])
	# Tomo la componente.
	g = t[1]
	# Busco el mapeo para 'path'.
	if maps_dict:
		map_info = maps_dict[g]
	# Convierto a 'path' en un string
	for i in range(0,len(t[0])):
		if i%2 == 0: # En los lugares pares estan los estados.
			if maps_dict:
				state_name_L = map_info[(str(pathL[i].left_state).partition('#'))[0]]
				state_name_R = map_info[(str(pathR[i].right_state).partition('#'))[0]]
			else:
				state_name_L = str(pathL[i].left_state)
				state_name_R = str(pathR[i].right_state)
			pathL[i] = '('+state_name_L+')'
			pathR[i] = '('+state_name_R+')'
		else: # En los lugares impares estan los eventos.
			pathL[i] = '"'+str(pathL[i])+'"'
			pathR[i] = '"'+str(pathR[i])+'"'
	separator = ' -> '
	r1 = separator.join(pathL)+'\t['+g.name+']'
	r2 = separator.join(pathR)+'\t['+g.name+']'
	return (r1,r2)

def graph (file):
	# Busco el ejecutable en el path.
	ltsgraph = ''
	if sys.platform == 'win32':
		for path in os.getenv('PATH').split(';'):
			if not path.endswith('\\'): path += '\\'
			path += "ltsgraph.exe"
			if os.path.isfile(path):
				ltsgraph = path
				break
	else:
		for path in os.getenv('PATH').split(':'):
			if not path.endswith('/'): path += '/'
			path += "ltsgraph"
			if os.path.isfile(path):
				ltsgraph = path
				break
	if not file.endswith('.aut'):
		file += '.aut'
	args = ["ltsgraph.exe", file]
	if ltsgraph != '':
		os.spawnv(os.P_NOWAIT, ltsgraph, args)

def from_file (file_name):
	"""
		Esta función lee de una archivo con formato '.aut' y construye un LTS.
	"""
	# Armo el nombre del archivo que contiene el sistema.
	if not file_name.endswith('.aut'):
		file_name += '.aut'
	# Armo el nombre del archivo que contiene el alfabeto.
	alphabet_file_name = file_name.replace('.aut','.alp')
	# Abro el archivo que contiene al LTS:
	try:
		f = open(file_name, 'r')
	except IOError:
		raise LTSError("File not found.", file_name)
	# Leo la primer linea que es de la fomra: "des(X,Y,Z)"
	data = f.readline()
	# Obtengo las cadenas X, Y, Z.
	init_state, transition_count, state_count = re.findall(r'\d+', data)
	# Creo el estado inicial.
	s0 = State(init_state, True)
	# Creo el LTS.
	result = LTS()
	# Si el alfabeto esta especifiado en un archivo lo cargo.
	exists_alphabet_file = False
	try:
		alphabet_file = open(alphabet_file_name, 'r')
	except IOError,(errno, strerror):
		if errno != 2: raise IOError(errno, strerror)
	else:
		data = '-'
		while data:
			data = alphabet_file.readline()
			data = data.replace('\n',' ').replace('\r',' ').replace('\t',' ')
			for e in data.split(' '):
				if e != '': result.add_event(e, e[0])
		exists_alphabet_file = True
		alphabet_file.close()
	# Agrego el estado inicial.
	result.add_state(s0)
	# Mientras haya lineas por leer, sigo leyendo.
	for i in range(0,int(transition_count)):
		# Leo la siguiente transicion del archivo.
		data = f.readline()
		# Si esta vacia vuelvo a la condicion para que salga del ciclo.
		if data == '': continue
		# Leo los nombres de los estados y del evento..
		data = data.replace('\n','').replace('\r','')
		data = data.replace('(','').replace(')','')
		data = data.replace(',"',';').replace('",',';')
		try: n_from, event, n_to = data.split(';')
		except: raise(LTSError("Syntax error in transition:", str(i+1)))
		if '#' in event:
			event = event.split('#')[0]
		# Me fijo si existen los estados, si no los agrego.
		s_from = State(n_from, False)
		s_to = State(n_to, False)
		if not result.is_state(s_from): result.add_state(s_from)
		else: s_from = result.get_state(s_from)
		if not result.is_state(s_to): result.add_state(s_to)
		else: s_to = result.get_state(s_to)
		# Agrego la transicion al LTS.
		result.add_transition(s_from, event, s_to)
		# Agrego el evento al alfabeto.
		result.add_event(event, event[0])
	# Cierro el archivo.
	f.close()
	# Le pongo un nombre al LTS.
	result.name = file_name
	# Si no tiene un archivo de alfabeto se crea uno.
	if not exists_alphabet_file:
		_generate_alphabet_file(result, file_name)
	return result

def to_file (lts, file_name=None):
	"""
		Esta función exporta el LTS a un archivo con formato '.aut'.
	"""
	# Nombre del archivo del sistema.
	if not file_name:
		file_name = lts.name
	if not file_name.endswith('.aut'):
		file_name += '.aut'
	# Creo el archivo donde se va a almacenar el LTS.
	f = open(file_name, 'w')
	# Obtengo el conjunto de transiciones.
	transition_set = lts.get_transition_set()
	# Obtengo la cantidad de estados.
	states = str(lts.get_state_count())
	# Obtengo la cantidad de transicion.
	transitions = str(len(transition_set))
	# Obtengo el estado inicial.
	s0 = lts.get_init_state()
	# Hago un mapeo entre los nombres de los estados y los Naturales dado que el
	# formato '.aut' solo acepta numeros como nombre de estados.
	map_info = dict()
	map_info[str(s0)] = '0'
	i = 1
	for x in lts.get_state_set():
		if not x.init:
			map_info[str(x)]= str(i)
			i += 1
	# Creo y escribo la primer linea del archivo.
	f.write('des(%s,%s,%s)\n'%(map_info[str(s0)],transitions,states))
	# Escribo las transiciones en el archivo.
	for t in transition_set:
		# Armo el string de la transicion.
		s = str(t[0]).partition('#')
		event_name = t[1]+s[1]+s[2]
		n_from = map_info[str(t[0])]
		n_to = map_info[str(t[2])]
		data = '(%s,"%s",%s)\n' % (n_from, event_name, n_to)
		f.write(data)
	f.close()
	# Guardo el alfabaeto.
	_generate_alphabet_file(lts)
	# Mapeo de estados.
	return map_info

def _generate_alphabet_file (lts, file_name=None):
	# Nombre del archivo que contiene el alfabeto.
	if not file_name:
		file_name = lts.name
	if not file_name.endswith('.aut'):
		alphabet_file_name = file_name+'.alp'
	else:
		alphabet_file_name = file_name.replace('.aut','.alp')
	# Creo el archivo que contiene el alfabeto.
	alphabet_file = open(alphabet_file_name, 'w')
	for e in lts.get_event_set('o'): alphabet_file.write(e+' ')
	alphabet_file.write('\n')
	for e in lts.get_event_set('u'): alphabet_file.write(e+' ')
	alphabet_file.write('\n')
	for e in lts.get_event_set('f'): alphabet_file.write(e+' ')
	alphabet_file.write('\n')
	for e in lts.get_event_set('c'): alphabet_file.write(e+' ')
	alphabet_file.write('\n')
	alphabet_file.close()
